(set-logic QF_AUFBV)
(set-info :source |These benchmarks are derived from a semi-automated proof of functional equivalence between two implementations of an Elliptic Curve Digital Signature Algorithm (ECDSA). More information about problem they encode can be found here: http://cps-vo.org/node/3405|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x55 () (_ BitVec 1))
(declare-fun x53 () (_ BitVec 1))
(declare-fun x52 () (_ BitVec 1))
(declare-fun x51 () (_ BitVec 384))
(declare-fun x50 () (_ BitVec 384))
(declare-fun x49 () (_ BitVec 1152))
(declare-fun x48 () (_ BitVec 768))
(declare-fun x47 () (_ BitVec 384))
(declare-fun x46 () (_ BitVec 384))
(declare-fun x45 () (_ BitVec 1152))
(declare-fun x44 () (_ BitVec 1))
(declare-fun x42 () (_ BitVec 1))
(declare-fun x41 () (_ BitVec 1))
(declare-fun x40 () (_ BitVec 384))
(declare-fun x39 () (_ BitVec 1152))
(declare-fun x38 () (_ BitVec 768))
(declare-fun x37 () (_ BitVec 384))
(declare-fun x36 () (_ BitVec 384))
(declare-fun x35 () (_ BitVec 384))
(declare-fun x34 () (_ BitVec 384))
(declare-fun x33 () (_ BitVec 1))
(declare-fun x32 () (_ BitVec 384))
(declare-fun x31 () (_ BitVec 1152))
(declare-fun x30 () (_ BitVec 384))
(declare-fun x29 () (_ BitVec 1152))
(declare-fun x28 ((_ BitVec 1152) (_ BitVec 768)) (_ BitVec 1152))
(declare-fun x27 () (_ BitVec 768))
(declare-fun x26 () (_ BitVec 384))
(declare-fun x25 () (_ BitVec 384))
(declare-fun x24 () (_ BitVec 1152))
(declare-fun x23 () (_ BitVec 384))
(declare-fun x22 () (_ BitVec 384))
(declare-fun x21 () (_ BitVec 384))
(declare-fun x19 () (_ BitVec 1))
(declare-fun x18 () (_ BitVec 1))
(declare-fun x17 () (_ BitVec 384))
(declare-fun x16 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x15 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x14 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x13 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x12 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x11 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x10 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x9 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x8 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x7 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x6 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x5 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x4 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x3 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x2 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x1 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x0 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun p56 () Bool)
(declare-fun p54 () Bool)
(declare-fun p43 () Bool)
(declare-fun p20 () Bool)
(assert (= p56 (and p43 p54)))
(assert (= x55 (bvand x42 x53)))
(assert (= p54 (or (= x17 (_ bv0 384)) (= x50 x51))))
(assert (= x53 (bvor x44 x52)))
(assert (= x52 (ite (= x50 x51) (_ bv1 1) (_ bv0 1))))
(assert (= x51 ((_ extract 383 0) x39)))
(assert (= x50 ((_ extract 383 0) x49)))
(assert (= x49 (x28 x45 x48)))
(assert (= x48 (concat x47 x46)))
(assert (= x47 (bvsub x34 x35)))
(assert (= x46 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x45 (concat x23 (concat x22 x21))))
(assert (= x44 (ite (= x17 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= p43 (or p20 (= x30 x40))))
(assert (= x42 (bvor x19 x41)))
(assert (= x41 (ite (= x30 x40) (_ bv1 1) (_ bv0 1))))
(assert (= x40 ((_ extract 383 0) x39)))
(assert (= x39 (x28 x31 x38)))
(assert (= x38 (concat x37 x32)))
(assert (= x37 (ite (= x17 (_ bv0 384)) (_ bv0 384) x36)))
(assert (= x36 (bvsub x34 x35)))
(assert (= x35 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x0 (_ bv11 4)) (select x0 (_ bv10 4))) (select x0 (_ bv9 4))) (select x0 (_ bv8 4))) (select x0 (_ bv7 4))) (select x0 (_ bv6 4))) (select x0 (_ bv5 4))) (select x0 (_ bv4 4))) (select x0 (_ bv3 4))) (select x0 (_ bv2 4))) (select x0 (_ bv1 4))) (select x0 (_ bv0 4)))))
(assert (= x34 (bvneg (_ bv340282367000166625977638945021017194497 384))))
(assert (= x33 (ite (= x17 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x32 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x31 (concat x23 (concat x22 x21))))
(assert (= x30 ((_ extract 383 0) x29)))
(assert (= x29 (x28 x24 x27)))
(assert (= x27 (concat x26 x25)))
(assert (= x26 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x0 (_ bv11 4)) (select x0 (_ bv10 4))) (select x0 (_ bv9 4))) (select x0 (_ bv8 4))) (select x0 (_ bv7 4))) (select x0 (_ bv6 4))) (select x0 (_ bv5 4))) (select x0 (_ bv4 4))) (select x0 (_ bv3 4))) (select x0 (_ bv2 4))) (select x0 (_ bv1 4))) (select x0 (_ bv0 4)))))
(assert (= x25 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert (= x24 (concat x23 (concat x22 x21))))
(assert (= x23 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x2 (_ bv11 4)) (select x2 (_ bv10 4))) (select x2 (_ bv9 4))) (select x2 (_ bv8 4))) (select x2 (_ bv7 4))) (select x2 (_ bv6 4))) (select x2 (_ bv5 4))) (select x2 (_ bv4 4))) (select x2 (_ bv3 4))) (select x2 (_ bv2 4))) (select x2 (_ bv1 4))) (select x2 (_ bv0 4)))))
(assert (= x22 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x3 (_ bv11 4)) (select x3 (_ bv10 4))) (select x3 (_ bv9 4))) (select x3 (_ bv8 4))) (select x3 (_ bv7 4))) (select x3 (_ bv6 4))) (select x3 (_ bv5 4))) (select x3 (_ bv4 4))) (select x3 (_ bv3 4))) (select x3 (_ bv2 4))) (select x3 (_ bv1 4))) (select x3 (_ bv0 4)))))
(assert (= x21 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv11 4)) (select x4 (_ bv10 4))) (select x4 (_ bv9 4))) (select x4 (_ bv8 4))) (select x4 (_ bv7 4))) (select x4 (_ bv6 4))) (select x4 (_ bv5 4))) (select x4 (_ bv4 4))) (select x4 (_ bv3 4))) (select x4 (_ bv2 4))) (select x4 (_ bv1 4))) (select x4 (_ bv0 4)))))
(assert (= p20 (not (= x17 (_ bv0 384)))))
(assert (= x19 (bvnot x18)))
(assert (= x18 (ite (= x17 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x17 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x0 (_ bv11 4)) (select x0 (_ bv10 4))) (select x0 (_ bv9 4))) (select x0 (_ bv8 4))) (select x0 (_ bv7 4))) (select x0 (_ bv6 4))) (select x0 (_ bv5 4))) (select x0 (_ bv4 4))) (select x0 (_ bv3 4))) (select x0 (_ bv2 4))) (select x0 (_ bv1 4))) (select x0 (_ bv0 4)))))
(assert true)
(assert (= (select x16 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x16 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x16 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x16 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x15 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x15 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x15 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x15 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x14 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x14 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x14 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x14 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x13 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x13 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x12 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x9 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x9 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x8 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x5 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x4 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv12 4)) (_ bv0 32)))
(assert (not (=> true p56)))
(check-sat)
(exit)
